1. Field of the Present Invention
The present invention is in the field of integrated circuit design and, more particularly, verifying the design of an integrated circuit prior to fabrication.
2. History of Related Art
In the field of integrated circuit design, formal verification refers to the process of rigorously proving that a design satisfies its specification. Typically, the specification of a verification problem includes a netlist-based representation of the design and a set of expected values for specified nets. As an example, a verification problem may include determining whether a state exists in which a CHECKSTOP signal is asserted, where an asserted CHECKSTOP signal indicates a fault. Using formal verification, one either finds a counterexample trace depicting a sequence of values of the nets over time, similar to a simulation trace, that leads to an assertion of the CHECKSTOP signal or proves that no such trace exists.
Formal verification is often performed using state space search algorithms. Such algorithms include unbounded and bounded exhaustive searches. Bounded exhaustive searches try to find an assertion of CHECKSTOP that can occur within N time steps from an initial state of the design. Unbounded exhaustive algorithms increase N until no states are encountered that have not already been encountered for smaller values of N (a condition termed “fixed-point”). If no path from an initial state to a violating state (a state in which CHECKSTOP is asserted) is encountered before fixed-point is reached, then correctness can be inferred.
The number of verification cycles required to perform an exhaustive state space search increases exponentially with the number of state holding elements or registers. This exponential relationship makes formal verification impractical for designs containing a very large number of state holding elements. As a result, semiformal verification have been employed as a verification technique suitable for large designs. Semiformal verification leverages formal algorithms by applying them to larger designees only in a resource-bounded manner. Semiformal verification, however, achieves only partial verification coverage. It would be desirable to implement a verification technique that facilitated the more complete verification coverage achievable with formal verification methods while addressing the resources limitations encountered when using formal verification.